nLab thunk-force category

Idea

A thunk-force category is a category that models call-by-value? programming languages with effects. More commonly, terms in a call-by-value language are modelled as morphisms in the Kleisli category of a strong monad. A thunk-force category axiomatizes the Kleisli category directly and is also called an abstract Kleisli category¹. The original category can be recovered from this category if it satisfies certain properties.

The name derives from programming terminology. A thunk means a value that represents an unevaluated computation, which can later be forced to be evaluated and perform its side effects. This is represented by the object $L A$ which could be read as a “thunk of $A$” or a “lazy $A$”. The thunking arrow $\theta_A : A \to L A$ embeds a value as a trivial thunk, and the force $\epsilon_A : L A \to A$ forces the evaluation of its thunked input.

The type constructor $L$ and associated thunk and force don’t normally appear as a standalone feature in a call-by-value language, but if the language supports first-class functions, they can be implemented in the usual way as a function of unit input. On the model side, this corresponds to the fact that if a thunk-force category is premonoidal closed, then $L A$ is equivalent to $I \rightharpoonup A$ and $\theta, \epsilon$ can be defined using this structure.

The opposite of a thunk-force category is sometimes called a category equipped with a runnable monad. (Thus, a thunk-force structure could be called a “(co)runnable comonad”, while a runnable monad could be called a “co-thunk-force category”.) Just as a thunk-force category models call-by-value programming, a runnable monad models call-by-name? programming.

Definition

A thunk-force category Führmann 99 consists of

• a category $K$
• a functor $L : K \to K$
• a possibly unnatural transformation $\theta : Id_K \to L$ pronounced thunk
• a natural transformation $\epsilon : L \to Id_K$ pronounced force

such that

• $(L\theta)\theta = (\theta L)\theta$
• $\theta L$ is a natural transformation
• $\epsilon\theta = \id$
• $(L\epsilon)(\theta L) = \id$

These conditions on the data $(L,\epsilon,\theta)$ can also be rephrased as

• $(L,\epsilon,\theta L)$ is a comonad.
• Each $\theta_A : A \to L A$ equips $A$ with the structure of an $L$-coalgebra over a comonad.

The second of these axioms states that $\epsilon\theta = \id$ and that $(L\theta)\theta = (\theta L)\theta$, while the first states that $\theta L$ is natural and $(L\epsilon)(\theta L) = \id$ (plus two other properties that follow from the second axiom).

The definition can be extended to monoidal closed thunk-force category to model a context and strong monad Führmann 99.

Thunkable Morphisms

A morphism $f : A \to B$ represents an effectful program. The presence of the thunk $\theta$ allows us to make the distinction between the “pure”/“trivially effectful” programs and those that have non-trivial effects. A morphism $f : A \to B$ in a thunk-force category is thunkable if $( L f )\theta = \theta f$, i.e., $\theta$ is “natural with respect to $f$”. Note that the condition $(L\theta)\theta = (\theta L)\theta$ in the definition says precisely that $\theta$ is thunkable.

The presence of non-thunkable morphisms makes $\theta$ fail to be natural overall; naturality of $\theta$ is exactly the same as saying all morphisms are thunkable. This is the case for the Kleisli category of the identity monad. On the other hand, most monads produce many non-thunkable morphisms. For example in the Kleisli category of the maybe monad, which is equivalent to the category of sets and partial functions, the thunkable morphisms are the total functions. As discussed below, most monads $T$ on a category $C$ used in denotational semantics satisfy an equalizing requirement which means the thunkable morphisms are in one-to-one correspondence to the morphisms of the original category $C$.

Relation to Monads

Let $(T,\eta,\mu)$ be a monad on a category $C$. The Kleisli category of $T$ is a thunk-force category. Let $F \dashv G$ denote the adjunction between $C$ and the Kleisli category $C_T$. Define $L = FG$ and $\epsilon$ the counit of the comonad. To define $\theta$, take $F\eta : F \to FT$ and, using the fact that $F$ is an identity-on-objects functor (or at least bijective on objects), treat it as an unnatural transformation from $Id_{C_T}\to L$. Then it follows immediately by naturality that every morphism in the image of $F$ is thunkable.

More explicitly, using the “Kleisli arrow” definition of the Kleisli category, $L$ is just $T$, $\epsilon_A : T A \to T A$ is the identity, and $\theta_A = \eta_{T A} \eta_{A} : A \to T^2 A$.

In the opposite direction, starting with a thunk-force category $K$, we can define the (non-full) subcategory of thunkable morphisms $G_\theta K$. Since $\theta L$ is natural, the image of $L$ lands in this subcategory, and is right adjoint to the inclusion. Then there is a monad $L_\theta$ induced on $G_{\theta}K$ by this adjunction. Furthermore, the thunk-force category generated by the Kleisli category of the monad is equivalent to $K$.

These constructions exhibit the category of thunk-force categories as a reflective subcategory of the category of monads. The subcategory can be characterized as the monads satisfying the “equalizing requirement”, that the unit $\eta$ of the monad is an equalizer in the following diagram:

$$1_{C}\underset{\quad \eta \quad}{\to}T\underoverset{\quad \eta T \quad}{T \eta}{\rightrightarrows}T^2$$

Which is in practice often satisfied for monads used in denotational semantics. The definition of the category of morphism of thunk-force categories and proof of this theorem are in Führmann 99 section 5.

Applications

Since the thunk $L$ is a comonad, the Kleisli category of the comonad is a model of a call-by-name? language. This is a semantic counterpart of the “thunking translation” of call-by-name into call-by-value (described for example in Hatcliff-Danvy 97.

Related Concepts

• The dual concept for call-by-name? is a runnable monad.
• A duploid is an analogous structure for effectful languages with both positive types and negative types.

References

Thunk-force categories were introduced (under the name “abstract Kleisli categories” in

• Carsten Führmann, “Direct Models of the Computational Lambda-calculus” Electronic Notes in Theoretical Computer Science 1999. https://doi.org/10.1016/S1571-0661(04)80078-180078-1)

See also:

• John Hatcliff and Olivier Danvy, “Thunks and the $\lambda$-Calculus”, Journal of Functional Programming 1997. https://doi.org/10.1017/S0956796897002748

---

1. We prefer the term thunk-force category since it is ambiguous whether Kleisli category refers to the Kleisli category of a monad or a comonad. ↩